Introduction in [Zantema - RTA'97]

Summary: ExIntrod_Zan97

• CS-TRS format
• OBJ format
• Negative results:
  1. CSRPO, Polynomials
  2. Lucas' transformation (Extra variables)
• Positive results:

CS-TRS ExIntrod_Zan97 (file ExIntrod_Zan97.csr)

Functions:  fact if zero s 0 prod p add true false

Constructors:  s 0 true false

Variables:  X Y

Arities: 

ar(fact) = 1
ar(if) = 3
ar(zero) = 1
ar(s) = 1
ar(0) = 0
ar(prod) = 2
ar(p) = 1
ar(add) = 2
ar(true) = 0
ar(false) = 0

Replacement map: 

µ(fact)={1}
µ(if)={1}
µ(zero)={1}
µ(s)={1}
µ(0)={}
µ(prod)={1,2}
µ(p)={1}
µ(add)={1,2}
µ(true)={}
µ(false)={}

Rules:  (file ExIntrod_Zan97)

fact(X) -> if(zero(X),s(0),prod(X,fact(p(X))))
add(0,X) -> X
add(s(X),Y) -> s(add(X,Y))
prod(0,X) -> 0
prod(s(X),Y) -> add(Y,prod(X,Y))
if(true,X,Y) -> X
if(false,X,Y) -> Y
zero(0) -> true
zero(s(X)) -> false
p(s(X)) -> X

The CS-TRS in OBJ format (file ExIntrod_Zan97.obj):

obj ExIntrod_Zan97 is
  sort S .
  op fact : S -> S .
  op if : S S S -> S [strat (1 0)] .
  op zero : S -> S .
  op s : S -> S .
  op 0 : -> S .
  op prod : S S -> S .
  op p : S -> S .
  op add : S S -> S .
  op true : -> S .
  op false : -> S .
  vars X Y : S .
  eq fact(X) = if(zero(X),s(0),prod(X,fact(p(X)))) .
  eq add(0,X) = X .
  eq add(s(X),Y) = s(add(X,Y)) .
  eq prod(0,X) = 0 .
  eq prod(s(X),Y) = add(Y,prod(X,Y)) .
  eq if(true,X,Y) = X .
  eq if(false,X,Y) = Y .
  eq zero(0) = true .
  eq zero(s(X)) = false .
  eq p(s(X)) = X .
endo

Negative results

1. The TRS is not simply mu-terminating [GL02b] for any replacement map greather than or equal to the canonical one, i.e.,

       µcan(fact)={}
       µcan(if)={1}
       µcan(zero)={1}
       µcan(s)={}
       µcan(0)={}
       µcan(prod)={1}
       µcan(p)={1}
       µcan(true)={}
       µcan(false)={}
       µcan(add)={1}
       

   The following µ-rewriting sequence in ExIntrod_Zan97 + Emb^µ(F)

       fact(s(0)) \-> if zero(s(0)) then s(0) else s(0)*fact(p(s(0)))
          \-> if false then s(0) else s(0)*fact(p(s(0)))
          \-> s(0)*fact(p(s(0)))
          \-> (0*fact(p(s(0))))+fact(p(s(0)))
          \-> 0+fact(p(s(0)))
          \-> fact(p(s(0)))
          \->_Embµ(F) fact(s(0))
          \-> ...
       

   shows that the TRS is not simply µ-terminating. Thus, in particular, no proof of µ-termination is possible by using CSRPO or polynomial interpretations.
2. The µ-termination of ExIntrod_Zan97 cannot be proved by using Lucas' transformation. The TRS ExIntrod_Zan97_L:

       fact(X) -> if(zero(X))
       add(0,X) -> X
       add(s(X),Y) -> s(add(X,Y))
       prod(0,X) -> 0
       prod(s(X),Y) -> add(Y,prod(X,Y))
       if(true) -> X
       if(false) -> Y
       zero(0) -> true
       zero(s(X)) -> false
       p(s(X)) -> X
       

   contains extra variables.

Positive results